i:Id, k:Knd, l:IdLnk, ds:x:Id fp Type, da:ltg:Knd fp Type,
f:(tg:Id(State(ds)Valtype(da;k)(da(rcv(l,tg))?Void List))) List.
@i: with declarations ds:dsda:da k(v) sends f s v on link l  Dsys 

latex

Definitions	Dsys, @i: with declarations ds:dsda:da k(v) sends f s v on link l, if b t else f fi, eqof(d), IdDeq, MsgA, with declarations ds:dsda:dak(v) sends f s v on link l, , State(ds), Valtype(da;k), f(x)?z, KindDeq, rcv(l,tg), a:A fp B(a), x:A. B(x), x. t(x), IdLnk, Knd, t  T, Id
Lemmas	Id wf, Knd wf, IdLnk wf, fpf wf, rcv wf, Kind-deq wf, fpf-cap wf, ma-valtype wf, ma-state wf, ma-empty wf, ma-single-sends wf, msga wf, id-deq wf, eqof wf, ifthenelse wf